Update to latest lean#16
Conversation
|
@srghma Thanks a lot for this patch! I'd love to welcome all sorts of updates like this :) Given that I haven't been involved in Lean 4 since a while ago (having lost most of my time to rustup) and I imagine a lot has changed to the language/libs since back then, I'd like to entrust you with the validity of this PR, as long as the CI passes XD |
| intro n ai; is_empty; intro ⟨a, i⟩; apply ai.false; exists a | ||
| cases i <;> trivial | ||
|
|
||
| def Lookup.lookup (Γ : Context) (x : Sym) : Decidable' (Σ a, Γ ∋ x ⦂ a) := by |
There was a problem hiding this comment.
I'd prefer keeping the last commit in a different PR from this one, since it seems to be working on a separate topic?
|
@rami3l done |
There was a problem hiding this comment.
@srghma Sorry, I still have the impression that you are redoing certain proofs rather than just migrating the code to a later version of Lean as suggested in the PR title...
To pick a simple example here, intro. is replaced with intro h; cases h whereas the deprecation warning clearly stated that it should be replaced with nofun.
Can you make the diff even smaller? I have done such migrations before and thus I believe most errors/warnings would only require minimal changes.
Also, I think it'd be better to absorb the changes in the feat: refactor based on review commit into the previous ones.
|
well, improved, but You tell make more minimal. at places I replaced by with ordinary functions bc there is no need to use by and ordinary funcs are easier to understand |
@srghma I agree on that particular point, thanks :) |
|
Thank You too can also propose to change to class and/or rename to PDecidable https://github.com/srghma/PLFaLean/blob/learning/Plfl/Init/PDecidable.lean ( I know before You named Decidable' as PDecidable :) ) P.S. will try to implement now everything in mm0 :) P.P.S. I live in Asia and ...hard to find job, dont know why. I want any - rust, ocaml, blockchain, full stack, etc. If You know some - can please help. If no - ignore :) just trying |
2 participants
No description provided.